Nuprl Lemma : map-map
11,40
postcript
pdf
as
:(top List),
f
,
g
:top. sqequal(map(
g
; map(
f
;
as
)); map(compose(
g
;
f
);
as
))
latex
Definitions
x
:
A
.
B
(
x
)
,
map(
f
;
as
)
,
compose(
f
;
g
)
,
Y
,
t
T
Lemmas
top
wf
origin
as:(top List), f,g:top. sqequal(map(g; map(f; as)); map(compose(g; f); as)) as:(top List), f,g:top. sqequal(map(g; map(f; as)); map(compose(g; f); as)) x:A. B(x)
T